00100	
00200	
00300	(DEFPROP FINI 
00400	 (LAMBDA(U R Z1 Z2 E)
00500	  (PROG (E1 N U1 R1 RES)
00550	(SETQ E(LAST E))(SETQ E1 E)(SETQ N(CONS Z1 Z2))
00600		(SETQ COUNT (PLUS COUNT (LENGTH R)))
00700	   A    (COND ((OR (GREATERP (NUM (CAR R)) LENGTH) (GREATERP (DEPTH (CDAR R)) DEPTH)) (GO B))
00800		      ((AND (EQ (NUM (CAR R)) 2) (TRIVDED (CAR R))) (GO B)))
01100		(SETQ U1 U)
01200	   E    (COND ((NOT (HERE(CAR U1))) NIL)
01250	   ((SUBSUME (CAR R) (CAR U1)) (DEL (CAR U1)) (GO C)))
01300		(SETQ U1 (CDR U1))
01400		(COND (U1 (GO E)))
01500		(SETQ RES (CONS (CAR R) RES))
01600	   B    (SETQ R (CDR R))
01700	   B1   (COND (R (GO A)))
01800	F1	(SETQ U1 U)
01900	   F    (COND ((NULL RES)(CLAUSES2 (CDR E)) (RETURN (LENGTH (CDR E)))))
02000	   G    (COND ((NOT(HERE(CAR U1))) NIL)((SUBSUME (CAR U1) (CAR RES)) (SETQ RES (CDR RES)) (GO F)))
02100		(SETQ U1 (CDR U1))
02200		(COND (U1 (GO G)))
02300		(RPLACD (CDAAR RES) (CONS 0 N))
02400		(SETQ R1 RES)
02500		(SETQ RES (CDR RES))
02600		(RPLACD R1 NIL)
02700		(RPLACD E1 R1)
02800		(SETQ E1 (CDR E1))
02900		(GO F1)
03000	   C    (SETQ U1 (CDR U1))
03100		(COND ((NULL U1) (GO D))((NOT(HERE(CAR U1)))(GO C))
03150	 ((SUBSUME (CAR R) (CAR U1)) (DEL (CAR U1))))
03200		(GO C)
03300	   D    (RPLACD (CDAAR R) (CONS 0 N))
03400		(SETQ R1 R)
03500		(SETQ R (CDR R))
03600		(RPLACD R1 NIL)
03700		(RPLACD E1 R1)
03800		(SETQ E1 (CDR E1))
03900		(GO B1))) 
04000	EXPR)